T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} .
(e':es-E(es). (es-le(es; e'; e)  ((es-when(es; x; e') = es-when(es; x; e)  T))))
 (x changed before e) 

latex

Definitions	P  Q, P  Q, A c B, prop{i:l}, P  Q, t  T, es-le(es; e; e'), P  Q, x:A. B(x), P  Q, EqDecider(T), x:A. B(x), False, ee'.P(e), decidable(P), A, es-dtype(es; i; x; T)
Lemmas	assert wf, iff wf, bool wf, event system wf, Id wf, es-dtype wf, es-E wf, es-loc wf, es-vartype wf, es-le-loc, es-when wf, not wf, es-locl wf, not-changed, changed wf, decidable assert